Nuprl Lemma : R-bframe-rule
11,40
postcript
pdf
i
:Id,
k
:Knd,
L
:(IdLnk List). Rbframe(
i
;
k
;
L
) ||-
es
.@
i
:
k
sends only on links in
L
latex
Definitions
t
T
,
True
,
P
Q
,
R-Feasible(
R
)
,
P
&
Q
,
R
||-
es
.
P
(
es
)
,
x
:
A
.
B
(
x
)
,
Consistent(
R
;
es
)
,
Lemmas
Id
wf
,
Knd
wf
,
IdLnk
wf
,
event
system
wf
,
Rbframe
wf
,
R-consistent
wf
origin
i:Id, k:Knd, L:(IdLnk List). Rbframe(i;k;L) ||- es.@i:k sends only on links in L i:Id, k:Knd, L:(IdLnk List). Rbframe(i;k;L) ||- es.@i:k sends only on links in L 
T
Qx:A. B(x)